/********************************
 * Robinson Matrix Algorithm
 *
 * Copyright (C) 2009 CNRS
 * Author : Florent AVELLANEDA, Eugen CEPOI
 * 
 *
 * All rights reserved.
 *
 *   This file is part of Robinson Matrix Algorithm.
 *
 *   Robinson Matrix Algorithm is free software: you can redistribute it and/or modify
 *   it under the terms of the GNU General Public License as published by
 *   the Free Software Foundation, either version 3 of the License, or
 *   (at your option) any later version.
 *
 *   Robinson Matrix Algorithm is distributed in the hope that it will be useful,
 *   but WITHOUT ANY WARRANTY; without even the implied warranty of
 *   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 *   GNU General Public License for more details.
 *
 *   You should have received a copy of the GNU General Public License
 *   along with Robinson Matrix Algorithm.  If not, see <http://www.gnu.org/licenses/>.
 *
 ***********************************************************************************/
#include "SAT.h"

#include <cassert>
#include <set>
#include <vector>
#include <iostream>
#include <map>

#include "Var.h"
#include "Clause.h"

#include "AlgoGraph.h"

namespace SAT
{
    SAT::SAT ( )
    {

    }

    SAT::~SAT ()
    {

    }

    void SAT::addClause( Clause c )
    {
        for (std::set< std::set< std::pair< Var*, bool > > >::iterator it = c._ssData.begin(); it != c._ssData.end(); ++it)
            for (std::set< std::pair< Var*, bool > >::iterator it2 = it->begin(); it2 != it->end(); ++it2)
            {
                if(_sVar.count( it2->first ) == 0)
                {
                    _sVar.insert( it2->first );
                    _vVar.push_back( it2->first );
                }
            }

        _Clause = _Clause * c; 
    }

    bool SAT::is2SatProblem()
    {
        for (std::set< std::set< std::pair< Var*, bool > > >::iterator it = _Clause._ssData.begin(); it != _Clause._ssData.end(); ++it)
            if( it->size() != 2 )
                return false;

        return true;
    }

    bool SAT::solve2Sat( )
    {
        // TODO : resoudre les conjonctions avec une seul variable pour rendre ces problemes 2-SAT
        assert( is2SatProblem() || !"Is not 2 SAT problem" );

        std::vector< std::set<unsigned int> > graph;
        graph.resize( _vVar.size()*2 );

        std::vector< std::set<unsigned int> > noGraph;
        noGraph.resize( _vVar.size()*2 );

        std::map<Var*, unsigned int> idPos;
        std::set<unsigned int> S;

        for (unsigned int i = 0; i < _vVar.size(); i++)
        {
            S.insert( i );
            idPos[ _vVar[i] ] = i;

            S.insert( i+_vVar.size() );
        }

        int idA, idB;
        std::set< std::pair<Var*, bool> >::iterator it2;
        for (std::set< std::set< std::pair< Var*, bool > > >::iterator it = _Clause._ssData.begin(); it != _Clause._ssData.end(); ++it)
        {
            it2 = it->begin();
            idA = idPos[it2->first] + (it2->second?0:_vVar.size());

            ++it2;

            idB = idPos[it2->first] + (it2->second?0:_vVar.size());

            graph[ (idB+_vVar.size())%(_vVar.size()*2) ].insert( idA );
            graph[ (idA+_vVar.size())%(_vVar.size()*2) ].insert( idB );


            noGraph[ idA ].insert( (idB+_vVar.size())%(_vVar.size()*2) );
            noGraph[ idB ].insert( (idA+_vVar.size())%(_vVar.size()*2) );
        }

        std::vector<unsigned int> result;
        result.resize(_vVar.size()*2);
        unsigned int nbS = AlgoGraph::stronglyConnected( graph, S, noGraph, result );

        {   // Tester si le probleme est satisfiable
            for (unsigned int i = 0; i < _vVar.size(); i++)
            {
                if( result[i] == result[i+_vVar.size()] )
                    return false; // pas de solution
            }
        }

        std::vector< std::set<unsigned int> > tabComp;
        tabComp.resize( nbS );
        for (unsigned int j = 0; j < result.size(); j++)
            tabComp[ result[j] ].insert(j);


        std::set<unsigned int> composanteNonEval;
        for (unsigned int j = 0; j < nbS; j++)
            composanteNonEval.insert( j );


        while(composanteNonEval.size() > 0)
            evaluerComposante( graph, *(composanteNonEval.rbegin()), true, composanteNonEval, tabComp, result );

        return true;
    }



    void SAT::evaluerComposante( std::vector< std::set<unsigned int> > &graph, unsigned int c, bool val, std::set<unsigned int> &composanteNonEval, std::vector< std::set<unsigned int> > &tabComp, std::vector<unsigned int> &composanteFC)
    {
        if( composanteNonEval.count( c ) == 0 )
            return;

        composanteNonEval.erase(c);


        for (std::set<unsigned int>::iterator it = tabComp[c].begin(); it != tabComp[c].end(); ++it)
        {
            if(*it < _vVar.size())
                _vVar[*it]->setVal(val);
            else
                _vVar[*it - _vVar.size()]->setVal(!val);

            if(val)
            {
                for (std::set<unsigned int>::iterator it2 = graph[*it].begin(); it2 != graph[*it].end(); ++it2)
                {
                    evaluerComposante( graph, composanteFC[ *it2 ], val, composanteNonEval, tabComp, composanteFC);
                }
            }

            evaluerComposante( graph, composanteFC[ (*it + _vVar.size()) % (_vVar.size()*2) ], !val, composanteNonEval, tabComp, composanteFC);
        }
    }




}
